es:ES, A:Type, Xs:(AbsInterface(A) List).
(f,gXs.  p-disjoint(E;f;g))
 (X:AbsInterface(A). (X  Xs)  (e:E. ((e  X))  (p-first(Xs)(e) = X(e)  A))) 

latex

Definitions	t  T, x:A. B(x), E, p-disjoint(A;f;g), Type, , AbsInterface(A), do-apply(f;x), p-first(L), <a, b>, s = t, X(e), e  X, ES, type List, x,y. t(x;y), (x,yL.  P(x;y)), (x  l), b, P  Q
Lemmas	do-apply-p-first-disjoint, assert wf, es-is-interface wf, l member wf, pairwise wf, es-interface wf, event system wf, p-disjoint wf, es-E wf